{--

    Courtesy of Philip Wadler.

    This is a port of Prof. Philip Wadlers pretty printer library to Frege.
    For more info see "http://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf"

 -}
{-
 * Author: Philip Wadler, Professor of Theoretical Computer Science
 *                        School of Informatics, University of Edinburgh
 * Ported to Frege: Ingo Wechsung
 *
 -}

package frege.lib.PP where

import frege.Prelude hiding(<+>, break)


infixr 9 `GROUP`  -- :<|>
infixr 6 `<>`
infixr 8 `<+>`
infixr 7 `</>` `<~/>` `<+/>`

data DOCUMENT = NONE
    | APPEND DOCUMENT DOCUMENT
    | NEST Int DOCUMENT
    | !TEXT String
    | LINE
    | GROUP DOCUMENT DOCUMENT
data Doc = None
    | Text {!hd  :: String, doc :: Doc}
    | Line {!ind :: Int, doc :: Doc}

nil = NONE

x <> y = APPEND x y
nest i x = NEST i x
text s = TEXT s
line = LINE
group x = flatten x `GROUP` x

flatten NONE = NONE
flatten (APPEND x y) = flatten x <> flatten y
flatten (NEST i x) = NEST i (flatten x)
flatten (t@TEXT s) = t
flatten LINE = TEXT ""
flatten (GROUP x y) = flatten x

layout' None = ""
layout' (Text s x) = s ++ layout' x
layout' (Line i x) = "\n" ++ blanks i ++ layout' x

layout doc = do
        sb <- StringBuilder.new ""
        layST sb doc
        sb.toString

native appendableFromWriter "(Appendable)" :: MutableIO Writer -> IOMutable Appendable

prettyIO :: MutableIO Writer -> Int -> DOCUMENT -> IO ()
prettyIO writer w doc = do
    app ← appendableFromWriter writer
    layST app (best w 0 doc)
    return ()

private layST ∷ Mutable a Appendable → Doc → STMutable a Appendable
private layST sb None = return sb
private layST sb (Text s x) = do
    sb.append s
    layST sb x
private layST sb (Line i x) = do
    sb.append "\n"
    sb.append (blanks i)
    layST sb x 

!blanks64 = packed (take 64 (repeat ' '))
private blanks 0 = ""
private blanks n 
        | n <= 64   = strhead blanks64 n
        | otherwise = blanks (n-64) ++ blanks64 

protected data PDOC = PDOC {!off :: Int, !doc :: DOCUMENT}      -- instead of (0,x)

best !w !k x = be w k [PDOC 0 x]
be !w !k [] = None
be !w !k (PDOC i (TEXT s):z) = s `Text` be w u z where !u = k+length s
be !w !k (PDOC i NONE:z) = be w k z
be !w !k (PDOC i (APPEND x y):z) = be w k (PDOC i x : PDOC i y : z)
be !w !k (PDOC i (NEST j x):z)   = be w k (PDOC u x : z) where u = i+j
be !w !k (PDOC i LINE:z) = i `Line` be w i z
be !w !k (PDOC i (GROUP x y):z)
    -- heuristic: only if we have not yet filled 2/3 of the space is the flattened version considered
    | k < 2*w `quot` 3   = case be w k (PDOC i x:z) of
        r | fits (w-k) r = r
          | otherwise    = be w k (PDOC i y : z)
    | otherwise = be w k (PDOC i y : z)

better w k x = if fits (w-k) x then Just x else Nothing

fits !w !x | w < 0 = false
fits w (Text s x) = fits (w - length s) x
fits _ _ = true
-- fits w None = true
-- fits w (Line i x) = true

pretty w x = ST.run (layout (best w 0 x))

-- utility functions

--- two documents with intervening space
NONE <+> y = y
x <+> y = x <> text " " <> y
--- two documents stacked
x </> y = x <> line <> y

folddoc f [] = nil
folddoc f [x] = x
folddoc f (x:xs) = f x (folddoc f xs)

--- some documents with space inbetween
spread = folddoc (<+>)
--- some documents stacked
stack  = folddoc (</>)
bracket l x r = group (block l x r)
block l x r = (text l <>
                        nest 2 (line <> x) <>
                        line <> text r)
--- join two documents without intervening space or stack them
x <~/> y = x <> (text "" `GROUP` line) <> y
--- join two documents with intervening space or stack them
NONE <+/> y = NONE <~/> y
x <+/> y = x <> (text " " `GROUP` line) <> y

fill [] = nil
fill [x] = x
fill (x:y:zs) = (flatten x <+> fill (flatten y : zs))
                `GROUP`
                (x </> fill (y : zs))

{-- like 'fill', but with separator between items -}
sep d [] = nil
sep d [x]  = x
sep d (x:y:zs) = (flatten (x <> text d) <+> sep d (flatten y  : zs))
                `GROUP`
                (x <> text d </> sep d (y:zs))

{-- like 'sep', but no space after separator -}
tight d [] = nil
tight d [x]  = x
tight d (x:y:zs) = (flatten (x <> text d) <> tight d (flatten y  : zs))
                `GROUP`
                (x <> text d </> tight d (y:zs))

--- fill words of a string
break s = (map text (´\s+´.splitted s))


--- turn a string into a document by breaking on space and filling up
msgdoc s = fill (break s)

listFromMaybe = Maybe.toList


